Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar1/HMSLASHt009.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

Q is empty.

↳ QTRS

  ↳ Non-Overlap Check

Q restricted rewrite system:
The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

Q is empty.

The TRS is non-overlapping. Hence, we can switch to innermost.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> BUSY₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b3, i3)
START₁(i) -> BUSY₇(F, closed, stop, false, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b2, i2)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b1, i1)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> BUSY₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b3, i3)
START₁(i) -> BUSY₇(F, closed, stop, false, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b2, i2)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b1, i1)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 1 SCC with 4 less nodes.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> BUSY₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> BUSY₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)

Used argument filtering: BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x7
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x7
newbuttons₄(x1, x2, x3, x4) = newbuttons₁(x4)
empty = empty
or₂(x1, x2) = x2
true = true
false = false
Used ordering: Precedence:

newbuttons₁ > true
empty > true

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPAfsSolverProof

                ↳ QDP

                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 1 SCC with 3 less nodes.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPAfsSolverProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)

Used argument filtering: BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x6
false = false
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x6
true = true
Used ordering: Precedence:

true > false

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPAfsSolverProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPAfsSolverProof

                        ↳ QDP

                          ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)

Used argument filtering: BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x5
false = false
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x5
true = true
Used ordering: Precedence:

true > false

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPAfsSolverProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPAfsSolverProof

                        ↳ QDP

                          ↳ QDPAfsSolverProof

                            ↳ QDP

                              ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)

Used argument filtering: BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x4
true = true
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x4
false = false
Used ordering: Precedence:

true > false

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPAfsSolverProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPAfsSolverProof

                        ↳ QDP

                          ↳ QDPAfsSolverProof

                            ↳ QDP

                              ↳ QDPAfsSolverProof

                                ↳ QDP

                                  ↳ QDPAfsSolverProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.

BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)

Used argument filtering: BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x2
closed = closed
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x2
open = open
Used ordering: Precedence:

open > closed

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPAfsSolverProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPAfsSolverProof

                        ↳ QDP

                          ↳ QDPAfsSolverProof

                            ↳ QDP

                              ↳ QDPAfsSolverProof

                                ↳ QDP

                                  ↳ QDPAfsSolverProof

                                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.